Uppaal Model Checker

UPPAAL
Developer(s)	Uppsala University Aalborg University
Initial release	1999 (1999)
Stable release	4.0.13 / September 27, 2010; 16 months ago (2010-09-27)
Preview release	4.1.13 / October 7, 2010; 16 months ago (2010-10-07)
Written in	C++ and GUI in Java
Operating system	Linux Mac OS X Microsoft Windows
Available in	English Danish Japanese Chinese Lithuanian
Type	Model checking
License	Commercial Licenses Academic Licenses
Website	http://www.uppaal.org/ http://www.uppaal.com/

Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays etc.).

The tool has been developed in collaboration between the Design and Analysis of Real-Time Systems group at Uppsala University, Sweden and Basic Research in Computer Science at Aalborg University, Denmark.

There are the following extensions available:

Cora for Cost Optimal Reachability Analysis.
Tron for Testing Real-time systems ON-line (black-box conformance testing).
Cover for COVERerage-optimal off-line test generation.
Tiga for TImed GAmes based controller synthesis.
Port for component based timed systems, exploiting Partial Order Reduction Techniques.
Pro for PRObabilistic reachability analysis.

Uppaal Model Checker

External links